(declare-sort S0 0)

(declare-sort S3 0)

(declare-fun _substvar_477_ () Int)
(declare-fun _substvar_479_ () Int)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const arr--2641678482790280333_-2641678482790280333-0 (Array Int Int))
(declare-const arr-541069142062511362_-2641678482790280333-0 (Array S0 Int))
(declare-const arr-2340543266927622224_-2641678482790280333-0 (Array (Array S0 Int) Int))
(declare-const arr-6203624965353714038_8234551869654487264-0 (Array (Array (Array S0 Int) Int) Bool))
(declare-const arr-8234551869654487264_541069142059263787-0 (Array Bool S3))
(declare-const arr-6203624965353714038_-4833119911203091970-0 (Array (Array (Array S0 Int) Int) (Array Bool S3)))
(declare-const arr-541069142059263787_3468333290027515575-0 (Array S3 (Array (Array S3 (Array (Array Int Int) (Array S0 Int))) S0)))
(declare-const arr--7760199855117383395_-4833119911203091970-0 (Array (Array S3 (Array (Array S3 (Array (Array Int Int) (Array S0 Int))) S0)) (Array Bool S3)))
(assert (or (xor true (distinct arr-6203624965353714038_8234551869654487264-0 (store arr-6203624965353714038_8234551869654487264-0 (store arr-2340543266927622224_-2641678482790280333-0 arr-541069142062511362_-2641678482790280333-0 (+ 0 i2 0 0 (* 4 (select arr--2641678482790280333_-2641678482790280333-0 0) (+ _substvar_477_ (+ i2 _substvar_479_ i4)) 4 4))) true)) true true true true true true true (< (select (store arr--2641678482790280333_-2641678482790280333-0 i2 0) 0) 0)) (= (select arr-6203624965353714038_-4833119911203091970-0 (store arr-2340543266927622224_-2641678482790280333-0 arr-541069142062511362_-2641678482790280333-0 i4)) arr-8234551869654487264_541069142059263787-0 (select arr--7760199855117383395_-4833119911203091970-0 arr-541069142059263787_3468333290027515575-0))))
(check-sat)
